\documentclass[10pt,spanish]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[spanish]{babel}
\usepackage[margin=1.0in]{geometry}
\usepackage{listings}
\usepackage[Algoritmo]{algorithm}
\usepackage{algorithmic}
\usepackage{graphicx}
\usepackage{float}
\lstset{language=Java,basicstyle=\tiny}

\renewcommand{\algorithmicrequire}{\textbf{Entrada:}}
\renewcommand{\algorithmicensure}{\textbf{Salida:}}

\parindent=0in
\parskip=8pt
\DeclareGraphicsExtensions{.pdf,.png,.jpg}

\begin{document}

\title{Implementación de GSAT en computación paralela}
\author{Ricardo Sansores, Oswaldo Rubio, Julio Mata}
\date{05/03/2012}

\maketitle

\begin{abstract}
\it Gran parte de los algoritmos no completos, usados para resolver el problema de satisfactibilidad, comienza con una asignación aleatoria de valores de verdad, para después moverlos mediante una heurística. Debido a que son algoritmos no completos, no podemos asegurar que la asignación aleatoria inicial conduzca a un resultado, por lo que la mayor parte de los algoritmos consideran reintentos. Dichos reintentos son completamente independientes uno de otro, lo que, en dado caso, permitiría ejecutarlos en paralelo, disminuyendo así el tiempo necesario para encontrar una solución.

Hemos elegido el algoritmo GSAT para hacer este análisi. Nuestra hipótesis es que, entre mayor sea el número de reintentos necesarios para encontrar la solución utilizando la versión secuencial del problema, deberíamos de obtener mejores tiempos de ejecución utilizando su versión paralela. Una restricción a esto es que funciona mejor para problemas grandes, ya que el cambio de contexto entre hilos, cuando se trata de problemas pequeños, incide más en el tiempo de ejecución total.

El presente documento exhibe una comparación entre los resultados obtenidos al resolver problemas de satisfactibilidad empleando algoritmos no completos tanto en sus versiones secuencial y paralela. Al final, compartimos nuestras observaciones y conclusiones al respecto.
\end{abstract}
\section{Introducción}
El problema de satisfactibilidad (SAT) se origina con la pregunta: Dada una fórmula proposicional, ¿tiene un modelo que la satisfaga? Usualmente el enfoque es en las fórmulas que están en forma clausal, esto es: donde las fórmulas son un conjunto de cláusulas, cada clásula es una disyunción de literales, y cada literal es una variable o su negación.

Los problemas así representados, en fórmulas clausales, se  identifican de la forma k-CNF, donde k es el número de literales.
Los problemas del tipo 2-CNF se resuelven en tiempo polinomial; los del tipo 3-CNF son NP-completos; esto es, que no hay un algoritmo determinista que en tiempo real pueda resolver el problema.

Ahora bien, ¿cómo se pueden resolver SAT?
Disponemos de los métodos sistemáticos, como las tablas de verdad y el procedimiento Davis Putnam; métodos de búsqueda local, como Greedy SAT (GSAT), WalkSAT, búsqueda en tabú; y métodos llamados ``exóticos'', como algoritmos genéticos y computación cuántica.

Los así llamados métodos exóticos la mayoría de las veces implican una complejidad innecesaria para resolver este tipo de problemas. Los métodos sistemáticos, como las tablas de verdad y el procedimiento Davis Putnam, son completos, pero su tiempo de ejecución para problemas grandes -o ``duros''- es muy largo, lo que los vuelve impracticables la mayoría de las veces. Los métodos de búsqueda local como GSAT y WalkSAT convierten este tipo de problemas ``duros''  en otros más manejables, que pueden ser solucionados en un tiempo polinomial.

En los últimos años el avance tecnológico ha permitido probar nuevas alternativas para resolver problemas de SAT de forma paralela. Los procesadores multicore \cite{cite_key4} y la posibilidad de utilizarlos de forma distribuida nos ayudan a evaluar dichas técnicas. Con estas pruebas podemos evaluar qué técnica nos conviene mas para resolver un problema. Algunas de las pruebas utilizando procesadores de forma paralela incluyen grids \cite{cite_key1} y plataformas que nos permiten conectar computadoras para compartir su poder de computo como BOINC \cite{cite_key3}, OpenMP y MPI \cite{cite_key6}. 

Sin embargo una de las técnicas más símples que podemos usar para aprovechar un procesador multicore es mediante el uso de programación multihilo  \cite{cite_key2}. En principio podemos pensar que mientras más hilos tengamos corriendo, tendrémos un mejor resultado. Pero también tenemos que tomar en cuenta que el beneficio de la paralelización tiene un costo: existe un límite \cite{cite_key7}, conocido como Ley de Amdhal \cite{cite_key5}. La Ley de Amdhal establece que a partir de cierto número de hilos, el desempeño no mejora sustancialmente.

\section{Algoritmos implementados de forma paralela}
\subsection{Algoritmo GSAT}
\begin{algorithm}[H]
\caption{Algoritmo GSAT}
\begin{algorithmic}

\REQUIRE un arreglo $A$ de cláusulas, $MAXFLIPS$ y $MAXTRIES$
\ENSURE un modelo (asignación de valores de verdad) que satisface $A$, si se encuentra

\STATE $cambiosRequeridos := 0$
\FOR{$i:=1$ to $MAXTRIES$}
	\STATE $V:=$ Una asignación aleatoria de valores de verdad 
	\FOR{$j:=1$ to $MAXFLIPS$}
		\IF{$V$ Es una solución válida}
			\STATE $cambiosEnUltimoIntento := j$
			\STATE $intentosRequeridos := i$
			\STATE $cambiosRequeridos := cambiosRequeridos + j$
			\RETURN $V$
		\ELSIF{$stopThread$}
			\RETURN $falso$
		\ENDIF
		\STATE cambiarValorGreedy()
	\ENDFOR
\ENDFOR
\RETURN $falso$
\end{algorithmic}
\end{algorithm}

\subsection{Paralelización}
En nuestra implementación específica de estos algoritmos, se especifica el número de ``threads'' (hilos de ejecución) que corren paralelamente. Al correr el programa, se crea un conjunto de ``resolucionadores'' que ejecutan en paralelo cada implementación del algoritmo. Todos ellos comparten una variable que indica si se ha llegado a una solución; cuando se ha alcanzado, se detiene el proceso y se reportan los resultados. 

La implementación del código paralelo es como sigue:
\begin{algorithm}[H]
\caption{Código Paralelo}
\begin{algorithmic}
\REQUIRE número de hilos $t$ a ejecutar
\ENSURE resultados de la ejecución
\STATE $t:=$número de threads
\STATE $datos \gets $ archivo de datos en forma CNF
\STATE $solvers:=$arreglo de resolucionadores de tamaño $t$
\FOR{$i:=1$ to $t$}
	\STATE Resolucionador $s \gets solvers[i]$
	\STATE $s.establecerParametros(datos, MAXTRIES, MAXFLIPS)$
	\STATE $s.iniciar()$	
\ENDFOR
\STATE Esperar hasta que los resolucionadores terminen intentos
\FOR{$i:=1$ to $t$}
	\STATE Resolucionador $s \gets solvers[i]$
	\STATE $s.detener()$	
\ENDFOR
\STATE Reportar tiempos
\RETURN Solución encontrada 
\end{algorithmic}
\end{algorithm}

\section{Parámetros a medir}
Los parámetros a considerar en la ejecución de los algoritmos son los siguientes:
\begin{itemize}
  \item \textbf{Tiempo de ejecución:} Es el tiempo que tardan en ejecutarse ambos algoritmos; éstos están implementados en el mismo lenguaje de programación y utilizan métodos comunes, de manera que podemos afirmar que la diferencia en tiempo de ejecución entre ellos será debido a la naturaleza de cada uno. 
  \item \textbf{Número de intentos máximos:} Ambos algoritmos tratan de llegar a un resultado, con distintos parámetros como delimitadores -flips en GSAT y $\Delta Temperatura$ en SA-SAT-. Éstos parámetros pueden detener la ejecución de cada algoritmo antes de obtener una respuesta -es por ello que son algoritmos no completos-; sin embargo, ambos algoritmos cuentan con un parámetro de reintentos. En caso de no obtener un resultado, se reintentará un número de veces definido.
  \item \textbf{Número de flips totales:} Aunque en el caso de GSAT el número de flips -veces que se cambia el valor de una propoción- es un delimitador, en el caso de SA-SAT también es usado éste parámetro pero únicamente como objeto de consulta.
  \item \textbf{Número de flips en el último intento:} A diferencia del número de flips totales, el número de flips en el último intento no es un parámetro acumulado durante la ejecución total del algoritmo. Éste parámetro indica el número de flips que se requirieron en el último intento, antes de obtener una solución.
  \item \textbf{¿Solución obtenida?:} Indica si el algoritmo logró llegar a una solución -un modelo que satisfaga la formula-.
  \item \textbf{Temperatura al momento de obtener el resultado:} Parámetro que únicamente se utiliza el algoritmo SA-SAT, pero que puede ser útil para detectar si hay un patrón que indique a que temperatura se suele obtener la solución.
\end{itemize}

\section{Hardware utilizado para las pruebas}

Para las pruebas utilizamos dos escenarios: 

\begin{itemize}
\item Un cluster cuyo acceso fue proporcionado por Intel Guadalajara; este cluster está formado por 16 nodos (192 núcleos); cada nodo tiene dos procesadores Intel Xeon 5670 a 2.93GHz con seis núcleos -doce en total-, memoria RAM de 1 GB 1066 MHz DDR3 y dos discos duros de 300 GB.
\item Un equipo de escritorio Intel i7 8 núcleos @ 1.6 GHZ 
\end{itemize}

\section{Resultados}
A continuación mostramos los resultados tanto en el cluster como en el equipo. En el eje X va el número de hilos, en el eje Y la magnitud -ya sea tiempo, intentos o cambios-, y cada serie representa un problema del conjunto de prueba de SATLIB.

Éstas son las gráficas del desempeño en el cluster:

\begin{figure}[H]
\caption{Gráfica de tiempos en el cluster}
\centering
\includegraphics[width=400pt]{grafTiempo}
\end{figure}

\begin{figure}[H]
\caption{Gráfica de intentos en el cluster}
\centering
\includegraphics[width=400pt]{grafIntentos}
\end{figure}

\begin{figure}[H]
\caption{Gráfica de flips en el cluster}
\centering
\includegraphics[width=400pt]{grafFlips}
\end{figure}

Como se puede apreciar en las gráficas del cluster, los valores van descendiendo conforme se aumenta el número de hilos. El resultado secuencial corresponderia al desempeño con un solo hilo. 

Y éstas las del desempeño en el equipo de escritorio:

\begin{figure}[H]
\caption{Gráfica de tiempos en el equipo}
\centering
\includegraphics[width=400pt]{grafTiempoLocal}
\end{figure}

\begin{figure}[H]
\caption{Gráfica de intentos en el equipo}
\centering
\includegraphics[width=400pt]{grafIntentosLocal}
\end{figure}

\begin{figure}[H]
\caption{Gráfica de flips en el equipo}
\centering
\includegraphics[width=400pt]{grafFlipsLocal}
\end{figure}

En cambio, en el equipo de escritorio el desempeño es más bien errático, debido a que el poder de computación es mucho menor que el cluster. 

En 2001 \cite{cite_key7} se hicieron pruebas similares utilizando algoritmos paralelos de SAT en un ambientes de computo de alto desempeño, obteniendo mejores resultados cuando son diseñados para ese tipo de ambientes.

\section{Conclusiones}

Los resultados en el cluster nos muestran que, en general, el tiempo disminuye drásticamente hasta los diez hilos; de ahí en adelante el comportamiento comienza a ser más o menos semejante. Se ven en particular dos problemas, el 2 y el 19, que tienen un comportamiento muy diferente a los otros. Lo mismo sucede para los intentos y los cambios de valores. 
 
El hecho de que a partir de alrededor diez hilos el desempeño no mejore significativamente tiene qué ver con la ley de Amdahl \cite{cite_key5}, que indica que la concurrencia está limitada por la naturaleza de la aplicación; tiene que ver con el tiempo que se realiza tanto en forma secuencial como en paralela.

Sean $s$ la fracción de tiempo secuencial intrínseco, $p$ el número de núcleos, $t_s$ el tiempo secuencial. El tiempo paralelo $T_p$ viene dado por:

$T_p = st_s + \frac{(1-s)t_s}{p}$

Una representación del tiempo serial y el tiempo paralelo puede apreciarse en la siguiente figura:

\begin{figure}[H]
\caption{Tiempos seriales y paralelos}
\centering
\includegraphics[width=200pt]{figAmdhalTiempo}
\end{figure}

Lo que significa que siempre habrá un tiempo serial que, aunque se incremente el número de hilos, siempre se presentará. Es por eso que a partir de cierto número de hilos, el desempeño ya no aumenta, por más hilos que se agreguen al algoritmo.

Finalmente si llegamos al enunciado de nuestra hipótesis, pero hay que tener en cuenta lo que establece la ley de Amdhal. 

\begin{thebibliography}{10}
 \bibitem[GridSAT]{cite_key1} W. Chrabakh, and R. Wolski, “GridSAT: A Chaff-basedDistributed SAT Solver for the Grid”, Proceedings of the ACM/IEEE
  Conference on Supercomputing, 2003.
  \bibitem[MultithreadingSAT]{cite_key2} Matthew Lewis, Tobias Schubert and Bernd Becker, "Multithreaded SAT Solving", 2007.
  \bibitem[BOINCSAT]{cite_key3} Michael Black and Gregory Bard, "SAT over BOINC: An Application-Independent Volunteer Grid Project", GRIDIEEE (2011) , p. 226-227.
  \bibitem[MulticoreSAT]{cite_key4} Alejandro Czutro, Bernd Becker and Ilia Polian, "Performance Evaluation of SAT-Based ATPG on Multi-Core
Architectures", Architecture of Computing Systems (ARCS), 2009 22nd International Conference.
  \bibitem[Amdahl]{cite_key5} Gene M. Amdahl, Validity of the single processor approach to achieving large scale computing capabilities, AFIPS spring joint computer conference, 1967.
  \bibitem [OpenMP/MPI]{cite_key6} Daniel Singer and Alain Vagner, "Parallel resolution of the satisfiability problem (SAT) with OpenMP and MPI". In Proceedings of the 6th international conference on Parallel Processing and Applied Mathematics (PPAM'05).
  \bibitem [AcceleratingSAT]{cite_key7} Ying Zhao, Sharad Malik, Matthew Moskewicz and Connor Madigan, "Accelerating Boolean Satisfiability through Application Specific Processing", System Synthesis, 2001.
\end{thebibliography}

\end{document}
